package sketch.specs.symbc;

import gov.nasa.jpf.symbc.Debug;

public class MyClassShort {
	
	public int myMethod(short x, short y) {
		int z = x + y;
		if (z > 100) {
			z = 1;
		} else {
			z = z - x;
		}
		z = x * z;
		return z;
	}
	
	// The test driver
	public static void main(String[] args) {
		MyClassShort mc = new MyClassShort();
		int x = mc.myMethod((short)1, (short)2);
		Debug.printPC("\nMyClass1.myMethod Path Condition: ");
	}
	
}